(op,id) lb  i < ub. E(i)
== if lb <z ub then (op,id) lb  i < ub - 1. E(i) op E(ub - 1) else id fi 
(recursive) 

latex

Up	groups 1
Wellformedness Lemmas	itop wf
Definitions	Y, if b then t else f fi , i <z j, x f y